\begin{tabbing}
$\forall$$A$, $B$:Realizer.
\\[0ex]R{-}Feasible($A$)
\\[0ex]$\Rightarrow$ R{-}Feasible($B$)
\\[0ex]$\Rightarrow$ $A$ $\parallel$ $B$
\\[0ex]$\Rightarrow$ \=($\forall$$k$:Knd.\+
\\[0ex]($\uparrow$isrcv($k$))
\\[0ex]$\Rightarrow$ (R{-}da($A$;source(lnk($k$)))($k$)?Void $\subseteq$r Valtype(R{-}da($B$;destination(lnk($k$)));$k$)))
\-
\end{tabbing}